#ifndef CFAIMPL_H
#define CFAIMPL_H
#include "prog.h"
#include "cfa.h"
#include <set>
#include <map>
#include <string.h>
using namespace std;
/*
x = e | x = id(e1, e2, ...) | return x
*/
struct UniNode: Node{
    Expr* e1;
    Expr* e2;
    char statement[256];
    //function call
    //char name[256];
    vector<Expr*> actualpara;
    Node *next;
    bool operator==(Node &other);
    StmtType st;
};
struct BinNode: Node{
    Prop *p;
    Node *_true, *_false;
    char statement[256];
    bool operator==(Node &other);
};
struct BadNode: Node{
    bool operator==(Node &other);
};
//CFA
struct NotMidterm{
    Node *first;
    Node *second;
};
//recursive building graph type
struct ProgramConnectType{
    Node *init;
    vector<Node**> ends1;
    vector<Node*> ends2;
    //check
};
class CFA_impl:public CFA{
    private:
        //function call
    	bool refined;
	char id[256];
	vector<VarExpr*> formal_parameter;
        //
        vector<Node*> LoopStart;
        vector<Node**> LoopEnd;
        //Lable Name
        map<Node*, char*> LabelSet;
        //origin
        Node* initNode;
        Node* finalNode;//BadNode

        Node* GetFinalNode(){ return finalNode; }
        void SetFinalNode(Node* X){ finalNode = X; }
        //write at x1.cc
        void RecursiveBinExpr(BinExpr*);
        InequProp* AssignExpr2Prop(Expr* , Expr*);
        //CFA(Prog)
//        ProgramConnectType BuildCFA(Prog, Node*, Node*, map<Node*, char*>*);
        void PrintSingleNodeWithGraphviz(ofstream&, Node*);
        //void PrintLogicType(LogicType);
        //void PrintProp(Prop*);
        //void PrintPropType(PropType);
        //void PrintOPType(OPType);
        void PrintBackNode(Node*);
        bool IsFound(vector<Node*> *, Node* );
        void RecursiveVerifyNode(Node*, set<Node*>&);
        void RecursiveVerifyNode(Node*, set<Node*>&, set<Node*>&);
        void RecursiveVerifyNode(Node*, set<Node*>&, vector<Expr*>&);
        //void RecursiveVerifyNode(Node*, set<Node*>&, map<Node*, Node*>&);
        void RecursiveVerifyNode(Node*, set<Node*>&, vector<NotMidterm>&);
        void RecursiveVerifyBackNode(Node*, set<Node*>&);
        void GraphOPType(ofstream&, OPType);
        void GraphLogicType(ofstream&, LogicType);
        void GraphPropType(ofstream&, PropType);
        void GraphExpr(ofstream&, Expr*);
        void GraphProp(ofstream&, Prop*);
        void GraphNodeUniNode(ofstream&, Node*);
        void GraphNode(ofstream&, Node*, set<Node*>&);
        void GraphNode1(ofstream&, Node*, set<Node*>&, int, int);
        void RecursiveGraphNode(ofstream&, Node*, set<Node*>&);
        void RecursiveGraphNode1(ofstream&, Node*, set<Node*>&, int, int);
        //connect goto
        void ConnectGoto(map<Node*, char*>*);
        void SetUniNodeStatement(Node*, int, char*);
        void SetInitNode(Node* X){ initNode = X; }
        void AddLableSet(pair<Node*, char*> p);
        void BuildGraph(int);
        //void PrintCFA();
        void PrintBackCFA();
        //refinement ywlee CFA
        bool CheckCFAValid(Node*);
        void RecursiveWalkNode(Node*, set<Node*>&);
        void RefineCFAywlee();
        void LabelReduction();
        void NotReplace();
    public:
	CFA_impl(){
		refined=false;
	}
        void setCFA( 
             vector<VarExpr*> i_formal_parameter, 
             map<Node*, char*> i_LabelSet, 
             Node* i_initNode,
             string Name);
        // at cfa.cc
        Node* GetInitNode(){ 
		if(!refined){
			printf("indeed refined\n");
			refined=true;
			LabelReduction();
			NotReplace();
		}
		return initNode; 
	} 
        char* GetId(){ return id; }//virtual GetFunctionName
        vector<VarExpr*> GetFormPara(){ return formal_parameter; }
        void AddFormPara(VarExpr* v){ formal_parameter.push_back(v); }
        map<Node*, char*> GetLableSet(){ return LabelSet; }
        void PrintCFA();
        void GetGlobalVariable(vector<Expr*>&);
        void SetId(char* name){ strcpy(id, name); }
        void CFA2Dot(const char*);
};
#endif
